(set-logic QF_LRA)
(set-info :source | Clock Synchronization. Bruno Dutertre (bruno@csl.sri.com) |)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(declare-fun x_0 () Real)
(declare-fun x_1 () Real)
(declare-fun x_2 () Real)
(declare-fun x_3 () Real)
(declare-fun x_4 () Real)
(declare-fun x_5 () Real)
(declare-fun x_6 () Real)
(declare-fun x_7 () Real)
(declare-fun x_8 () Real)
(declare-fun x_9 () Real)
(declare-fun x_10 () Real)
(declare-fun x_11 () Real)
(declare-fun x_12 () Real)
(declare-fun x_13 () Real)
(declare-fun x_14 () Real)
(declare-fun x_15 () Real)
(declare-fun x_16 () Real)
(declare-fun x_17 () Real)
(declare-fun x_18 () Real)
(declare-fun x_19 () Real)
(declare-fun x_20 () Real)
(declare-fun x_21 () Real)
(declare-fun x_22 () Real)
(declare-fun x_23 () Real)
(declare-fun x_24 () Real)
(declare-fun x_25 () Real)
(declare-fun x_26 () Real)
(declare-fun x_27 () Real)
(assert (let ((?v_21 (<= x_7 x_12)) (?v_25 (<= x_10 x_12)) (?v_9 (= x_19 x_12)) (?v_10 (= x_20 x_12))) (let ((?v_15 (not ?v_9)) (?v_18 (not ?v_10)) (?v_8 (+ (+ x_12 x_13) x_14))) (let ((?v_22 (= x_19 ?v_8)) (?v_26 (= x_20 ?v_8))) (let ((?v_35 (not ?v_22))) (let ((?v_29 (and ?v_21 ?v_35)) (?v_36 (not ?v_26))) (let ((?v_32 (and ?v_25 ?v_36)) (?v_2 (- x_1 x_6)) (?v_3 (- x_7 x_8)) (?v_4 (- x_2 x_9)) (?v_5 (- x_10 x_11)) (?v_6 (- x_12 x_17)) (?v_7 (- x_12 x_18)) (?v_11 (- x_1 x_4)) (?v_12 (- x_7 x_21)) (?v_13 (- x_2 x_5)) (?v_14 (- x_10 x_22)) (?v_16 (- x_1 x_23)) (?v_17 (- x_7 x_12)) (?v_19 (- x_2 x_24)) (?v_20 (- x_10 x_12)) (?v_30 (- x_23 x_4))) (let ((?v_23 (* ?v_30 1000)) (?v_24 (* (- x_23 x_5) 1000)) (?v_27 (* (- x_24 x_4) 1000)) (?v_33 (- x_24 x_5))) (let ((?v_28 (* ?v_33 1000)) (?v_31 (- x_12 x_21)) (?v_34 (- x_12 x_22)) (?v_37 (- x_6 x_23)) (?v_39 (- x_9 x_24)) (?v_0 (+ x_0 (/ 1001 1000))) (?v_1 (+ x_3 (/ 1001 1000))) (?v_38 (* (* x_14 999) (/ 1 1000))) (?v_40 (* (* x_14 1001) (/ 1 1000))) (?v_41 (+ (+ (+ x_15 x_16) (* (* (+ x_17 x_14) 2) (/ 1 999))) (/ 2335 666)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (<= x_13 0)) (not (<= x_14 0))) (not (<= x_15 0))) (not (< x_16 (+ x_15 (* (* (+ (* (* x_14 1) (/ 1 2)) 1) 1001) (/ 1 999)))))) (< x_17 (- (* (* (- (- x_14 x_16) 1) 999) (/ 1 2)) 1))) (not (< x_17 (* (* (+ (+ (+ x_13 x_15) x_16) (/ 1501 1000)) 1001) (/ 1 999))))) (not (<= x_18 0))) (<= x_18 (- x_13 (+ (+ x_15 (* (* (+ x_14 2) 1001) (/ 1 999))) (/ 1 2))))) (<= x_0 x_1)) (<= x_0 x_2)) (<= x_1 ?v_0)) (<= x_2 ?v_0)) (<= x_3 x_4)) (<= x_3 x_5)) (<= x_4 ?v_1)) (<= x_5 ?v_1)) (<= (* (* ?v_3 999) (/ 1 1000)) ?v_2)) (<= (* (* ?v_5 999) (/ 1 1000)) ?v_4)) (<= ?v_2 (* (* ?v_3 1001) (/ 1 1000)))) (<= ?v_4 (* (* ?v_5 1001) (/ 1 1000)))) (<= ?v_6 x_21)) (<= ?v_6 x_22)) (<= x_21 ?v_7)) (<= x_22 ?v_7)) (<= (- x_21 x_21) x_16)) (<= (- x_22 x_21) x_16)) (<= (- x_21 x_22) x_16)) (<= (- x_22 x_22) x_16)) (or (and ?v_9 (<= x_7 x_25)) ?v_22)) (or (and ?v_10 (<= x_10 x_25)) ?v_26)) (or ?v_9 ?v_10)) (or ?v_15 (and (<= (* (* ?v_12 999) (/ 1 1000)) ?v_11) (<= ?v_11 (* (* ?v_12 1001) (/ 1 1000)))))) (or ?v_18 (and (<= (* (* ?v_14 999) (/ 1 1000)) ?v_13) (<= ?v_13 (* (* ?v_14 1001) (/ 1 1000)))))) (or (or ?v_15 ?v_21) (and (and (not (< x_0 x_23)) (<= (* (* ?v_17 999) (/ 1 1000)) ?v_16)) (<= ?v_16 (* (* ?v_17 1001) (/ 1 1000)))))) (or (or ?v_18 ?v_25) (and (and (not (< x_0 x_24)) (<= (* (* ?v_20 999) (/ 1 1000)) ?v_19)) (<= ?v_19 (* (* ?v_20 1001) (/ 1 1000)))))) (or ?v_29 (and (<= x_26 (+ (+ (* (* (+ (+ (+ x_21 (* ?v_23 (/ 1 999))) x_22) (* ?v_24 (/ 1 999))) 1) (/ 1 2)) x_15) (/ 3001 1998))) (not (< x_26 (- (- (* (* (+ (+ (+ x_21 (* ?v_23 (/ 1 1001))) x_22) (* ?v_24 (/ 1 1001))) 1) (/ 1 2)) x_15) (/ 1 2))))))) (or ?v_32 (and (<= x_27 (+ (+ (* (* (+ (+ (+ x_21 (* ?v_27 (/ 1 999))) x_22) (* ?v_28 (/ 1 999))) 1) (/ 1 2)) x_15) (/ 3001 1998))) (not (< x_27 (- (- (* (* (+ (+ (+ x_21 (* ?v_27 (/ 1 1001))) x_22) (* ?v_28 (/ 1 1001))) 1) (/ 1 2)) x_15) (/ 1 2))))))) (or ?v_29 (and (<= (* (* ?v_31 999) (/ 1 1000)) ?v_30) (<= ?v_30 (* (* ?v_31 1001) (/ 1 1000)))))) (or ?v_32 (and (<= (* (* ?v_34 999) (/ 1 1000)) ?v_33) (<= ?v_33 (* (* ?v_34 1001) (/ 1 1000)))))) (or ?v_35 (= x_8 (+ x_26 x_14)))) (or ?v_36 (= x_11 (+ x_27 x_14)))) (or ?v_35 (and (<= ?v_38 ?v_37) (<= ?v_37 ?v_40)))) (or ?v_36 (and (<= ?v_38 ?v_39) (<= ?v_39 ?v_40)))) (= x_25 (+ x_12 x_14))) (or (or (or (not (<= (- x_7 x_7) ?v_41)) (not (<= (- x_10 x_7) ?v_41))) (not (<= (- x_7 x_10) ?v_41))) (not (<= (- x_10 x_10) ?v_41)))))))))))))
(check-sat)
(exit)
